a:{...0}, b:. (a  b) = (-((-a)  b)) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), False, P  Q, A, a  b  T , , True, T, {...i}, P & Q, P  Q, i > j, i  j , A  B, , S  T
Lemmas	int lower wf, nat plus wf, rem bounds 2, rem bounds 1, nat plus inc int nzero, div rem sum, add mono wrt eq, gt wf, ge wf, le wf, true wf, squash wf, add mono wrt lt, add mono wrt le, lt transitivity 1, mul cancel in lt